perm filename NOTES.THE[LSP,JRA] blob sn#254381 filedate 1976-12-17 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	To describe the evaluation of a function-call in LISP we must add
C00007 00003	.NEXT PAGE
C00021 ENDMK
C⊗;
To describe the evaluation of a function-call in LISP we must add
an equation to %9D%4e%1:
.BEGIN  TABIT1(15);FILL;TURN ON "#";

\%9D%4e%f(%af%1[%as%41%1,#...,%as%4n%1]%f)%d(l)%1#=#
%9D%4a%f(%af%f)%d(l)(%9D%4e%f(%as%41%f)%d(l)%1,#...,%9D%4e%f(%as%4n%f)%d(l))%1
.END
We must also make consistent modifications to the previous clauses of %9D%4tgr%1 to
account for environments.
That is, the value of a constant is independent of the
specific environment in which it is evaluated. 
.BEGIN TURN OFF "{","}";TURN ON "#";center;
%9D%4e%1{%as%*}(%dl%*)#=#%ds%*. 

.END
A similar  modification must be made for
conditional expressions.

Before we get very far in applying functions to values
we must give a mathematical characterization of function definitions.
In this section we will handle
 handle λ-notation without free variables, postponing more complex
cases to {yonss(P90)}.

Assuming the only free variables in %9x%* are among the %3x%4i%*'s
the denotation of %3λ[[x%41%*, ..., x%4n%*] %9x%1] in a specified
environment should be a function 
from %aS%8n%1 to %aS%* such that:
.BEGIN TABIT1(15);FILL;TURN ON "#";

\%9D%4a%f(%3λ[[%av%41%1,#...#%av%4n%1]%as%1]%f)%d(l)%1#=#
%d%9λ%d(x%41%*,#...,#%dx%4n%*)%9D%4e%f(%as%f)%d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1
.END

where λ is the LISP λ-notation and %9λ%* is its mathematical counterpart and
%dv%4i%1 is the denotational counterpart of %av%4i%1.

In more detail:
%9λ%d(x%41%*, ... ,x%4n%*)e(x%41%*, ... ,x%4m%*) %1is a function %df%*: %aS%8n%1 → %aS%* such that:

.BEGIN TABIT1(15);GROUP;

\ | is %de(t%41%*, ... ,t%4n%*) %1if m%c≥%*n and %c∀%*i%dt%4i%1 %c≠%* %9B%1.
%df(t%41%*, ... t%4m%*)  %1\<
\ | is %9B%* otherwise

.END
Also, %d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1 is a modification
of %dl%* such that each %dv%4i%1 is bound to  the corresponding %dx%4i%1.

.BEGIN TABIT2(20,40);GROUP;
That is:\%d(l#:#<x,v>)%1 is: %9λ%d(v%41%*)%2\if %dv = %9B%* %2then %9B%2 
\\else if %dv%41%* = %9B%2 then %9B%2
\\else if %dv%41%* = x%2 then %dv%2
\\else %dl(v%41%*)%1.

where: %2if%d p%* then %dq%* else %dr%1  is  %dif(p,q,r)%1.
.END

After all this work there really should be a comparable return on
on our investment. An immediate benefit is
clearer understanding of the differences between mathematics and programming
languages and a
 clearer perception of the role of definition and computation.
 It should raise questions about the class of objects called function
and the class of objects called procedures.

We know that the LISP %3label%1 operator is similar to "<=", but
%3label%1 builds a temporary definition, while "<=" modifies the
environment. Programming language constructs which modify the environment
are said to have %2side-effects%1 and  are an instance
of what is called a imperative construct.
The next chapter introduces the procedural aspects of 
imperative constructs and  in {yonss(P90)}
we will investigate some of the mathematical aspects of
"<=" and %3label%1.


.NEXT PAGE;
.<<to raproachment???>>
We can give some insight into the mathematical properites of
%3label%1.
As before, we take our clues from the behavior of %3eval%* and %3apply%*.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the 
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation 
%df(t%4i%*,#...,#t%4n%*)#=#%dg(t%4i%*,#...,#t%4n%*)%1.
So:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l)%1.
.END

This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
We must be a bit careful.
Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
rather than when
 the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation 
should be a mapping like: %denv%*#→#[%aS%8n%1#→#%aS%*] rather than
simply %aS%8n%1#→#%aS%1. This is consistent with our understanding of the
meaning of λ-notation.
It is what %3function%* was attempting to 
describe. 
What we previously have called an ⊗→open function↔← is  of the
form: 
 %aS%8n%1#→#%aS%*.

.END
 This view of λ-notation must change our conception on %denv%* as well.
Given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. That is, for such names:

.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%1 → [%denv%1 → %aFn%1]
.END

A modification of our handling of %3label%* seems to describe the case 
for recursion:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l#:#<f,%9D%4a%f(%ag%f)%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.

Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; %et%3 → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation and will return  a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it imposes the minimal structure on the function⊗↓Like 
a free group satisfies the group axioms, but imposes no other
requirements.←.
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. This discussion of "least" brings in the recent work of D. Scott
and  the intuition behind
this study  again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).

Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; %et%3 → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%9B%*>,<1,%9B%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%9B%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %dn%82%1 on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %9B%1 if %di%c<%dn

.END

We may think of our "equation-solver" as proceeding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is 
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.


In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) cond(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %9B%*#⊗↓We 
perhaps should subscript %9B%* to distinguish it from previous %9B%*'s.←.


.BEGIN CENTER;
%9t%d(%9B%d) = %9λ%d((n) cond(n=0, 0, %9B%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%9B%*)%1 is just %df%41%1!
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%9B%*))#=#%9λ%d((n) cond(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %9B%1.← we can say
.BEGIN CENTER;GROUP;

%df%4n%* = %9t%8n%d(%9B%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4n=0 → ∞%9t%8n%d(%9B%d)%1.
.END

Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4n→∞%9t%8n%d(%9B%d).%1
.END
Thus in summary, %dY%* is a mapping: %d[[%aFn%* → %aFn%*] → %aFn%*]%1
such that if %9t%*#%9ε%d#[%aFn%*#→#%aFn%*]%1 and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1 and %dY(%9t%*)%1 is least-defined of any of the solutions
to %df%*#=#%9t%d(f)%1.
.END

So the search for denotations for %3label%* might be better served by:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%f(%ag%f)%d(l%1#:#%d<f,h>))%1.
.END


The characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%f(%3label[car;car][(A#B)]%f)%1 will exhibit a discrepancy.
Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by  the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %df#=#g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two  denotations different? 
And which, if either, interpretation is %2correct%*? 
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?

The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.


The intuitions presented in this section can be made very  precise. 
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
Indeed, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.

*** ADD MONOTONICITY, CONTINUITY

***** continuations and models for imperatives****